Termination proof of /tmp/tmp9W

Termination of the given ITRSProblem could not be shown:

↳ ITRS

  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

if(FALSE, u, v) → v
if(TRUE, u, v) → u
minusNat(TRUE, x, y) → minus(x, round(y))
minus(x, y) → minusNat(&&(>=@z(y, 0@z), =@z(x, +@z(y, 1@z))), x, y)
round(x) → if(=@z(%@z(x, 2@z), 0@z), x, +@z(x, 1@z))

The set Q consists of the following terms:

if(FALSE, x0, x1)
if(TRUE, x0, x1)
minusNat(TRUE, x0, x1)
minus(x0, x1)
round(x0)

Added dependency pairs

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

if(FALSE, u, v) → v
if(TRUE, u, v) → u
minusNat(TRUE, x, y) → minus(x, round(y))
minus(x, y) → minusNat(&&(>=@z(y, 0@z), =@z(x, +@z(y, 1@z))), x, y)
round(x) → if(=@z(%@z(x, 2@z), 0@z), x, +@z(x, 1@z))

The integer pair graph contains the following rules and edges:

(0): MINUS(x[0], y[0]) → MINUSNAT(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))), x[0], y[0])
(1): MINUSNAT(TRUE, x[1], y[1]) → MINUS(x[1], round(y[1]))
(2): ROUND(x[2]) → IF(=@z(%@z(x[2], 2@z), 0@z), x[2], +@z(x[2], 1@z))
(3): MINUSNAT(TRUE, x[3], y[3]) → ROUND(y[3])

(0) -> (1), if ((x[0] →^* x[1])∧(y[0] →^* y[1])∧(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))) →^* TRUE))

(0) -> (3), if ((x[0] →^* x[3])∧(y[0] →^* y[3])∧(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))) →^* TRUE))

(1) -> (0), if ((round(y[1]) →^* y[0])∧(x[1] →^* x[0]))

(3) -> (2), if ((y[3] →^* x[2]))

The set Q consists of the following terms:

if(FALSE, x0, x1)
if(TRUE, x0, x1)
minusNat(TRUE, x0, x1)
minus(x0, x1)
round(x0)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

if(FALSE, u, v) → v
if(TRUE, u, v) → u
round(x) → if(=@z(%@z(x, 2@z), 0@z), x, +@z(x, 1@z))

(0) -> (1), if ((x[0] →^* x[1])∧(y[0] →^* y[1])∧(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))) →^* TRUE))

(0) -> (3), if ((x[0] →^* x[3])∧(y[0] →^* y[3])∧(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))) →^* TRUE))

(1) -> (0), if ((round(y[1]) →^* y[0])∧(x[1] →^* x[0]))

(3) -> (2), if ((y[3] →^* x[2]))

The set Q consists of the following terms:

if(FALSE, x0, x1)
if(TRUE, x0, x1)
minusNat(TRUE, x0, x1)
minus(x0, x1)
round(x0)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

if(FALSE, u, v) → v
if(TRUE, u, v) → u
round(x) → if(=@z(%@z(x, 2@z), 0@z), x, +@z(x, 1@z))

The integer pair graph contains the following rules and edges:

(1): MINUSNAT(TRUE, x[1], y[1]) → MINUS(x[1], round(y[1]))
(0): MINUS(x[0], y[0]) → MINUSNAT(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))), x[0], y[0])

(0) -> (1), if ((x[0] →^* x[1])∧(y[0] →^* y[1])∧(&&(>=@z(y[0], 0@z), =@z(x[0], +@z(y[0], 1@z))) →^* TRUE))

(1) -> (0), if ((round(y[1]) →^* y[0])∧(x[1] →^* x[0]))

The set Q consists of the following terms:

if(FALSE, x0, x1)
if(TRUE, x0, x1)
minusNat(TRUE, x0, x1)
minus(x0, x1)
round(x0)

Represented integers and predefined function symbols by Terms

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], round(y[1]))
MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])

The TRS R consists of the following rules:

if(false, u, v) → v
if(true, u, v) → u
round(x) → if(equal_int(mod_int(x, pos(s(s(0)))), pos(0)), x, plus_int(pos(s(0)), x))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(pos(x), neg(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
mod_int(neg(x), neg(y)) → neg(mod_nat(x, y))
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
if1(true, x, y) → x
if1(false, x, y) → y
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(0), neg(y)) → true
greatereq_int(pos(x), neg(y)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(neg(x), pos(s(y))) → false
greatereq_int(neg(s(x)), pos(0)) → false
greatereq_int(neg(s(x)), neg(0)) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
greatereq_int(neg(s(x)), neg(s(y))) → greatereq_int(neg(x), neg(y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
minusNat(true, x0, x1)
minus(x0, x1)
round(x0)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], round(y[1]))
MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
round(x) → if(equal_int(mod_int(x, pos(s(s(0)))), pos(0)), x, plus_int(pos(s(0)), x))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
minusNat(true, x0, x1)
minus(x0, x1)
round(x0)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

minusNat(true, x0, x1)
minus(x0, x1)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], round(y[1]))
MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
round(x) → if(equal_int(mod_int(x, pos(s(s(0)))), pos(0)), x, plus_int(pos(s(0)), x))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
round(x0)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, x[1], y[1]) → MINUS(x[1], round(y[1])) at position [1] we obtained the following new rules [LPAR04]:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])
MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))

The TRS R consists of the following rules:

greatereq_int(pos(x), pos(0)) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), pos(0)) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
round(x) → if(equal_int(mod_int(x, pos(s(s(0)))), pos(0)), x, plus_int(pos(s(0)), x))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
round(x0)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])
MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
round(x0)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

round(x0)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0])
MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables pos(s(s(0))) is replaced by the fresh variable x_removed.
Pair: MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
Positions in right side of the pair:

[1,0,0,1]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                        ↳ QDP

                                      ↳ RemovalProof

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MINUS(x[0], y[0], x_removed) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0], x_removed)
MINUSNAT(true, x[1], y[1], x_removed) → MINUS(x[1], if(equal_int(mod_int(y[1], x_removed), pos(0)), y[1], plus_int(pos(s(0)), y[1])), x_removed)

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

[1,0,0,1]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                        ↳ QDP

                                      ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MINUS(x[0], y[0], x_removed) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0], x_removed)
MINUSNAT(true, x[1], y[1], x_removed) → MINUS(x[1], if(equal_int(mod_int(y[1], x_removed), pos(0)), y[1], plus_int(pos(s(0)), y[1])), x_removed)

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule MINUS(x[0], y[0]) → MINUSNAT(and(greatereq_int(y[0], pos(0)), equal_int(x[0], plus_int(pos(s(0)), y[0]))), x[0], y[0]) at position [0] we obtained the following new rules [LPAR04]:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, plus_int(pos(s(0)), neg(s(x0))))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), pos(x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), neg(0)))), y0, neg(0))
MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, plus_int(pos(s(0)), neg(s(x0))))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), pos(x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), neg(0)))), y0, neg(0))
MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, plus_int(pos(s(0)), neg(s(x0))))), y0, neg(s(x0))) at position [0,1,1] we obtained the following new rules [LPAR04]:

MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), pos(x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), neg(0)))), y0, neg(0))
MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0)))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), pos(x0)))), y0, pos(x0)) at position [0,1,1] we obtained the following new rules [LPAR04]:

MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), neg(0)))), y0, neg(0))
MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, plus_int(pos(s(0)), neg(0)))), y0, neg(0)) at position [0,1,1] we obtained the following new rules [LPAR04]:

MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, pos(x1)) → MINUSNAT(and(greatereq_int(pos(x1), pos(0)), equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1)) at position [0,0] we obtained the following new rules [LPAR04]:

MINUS(y0, pos(x1)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x1)))), y0, pos(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(s(0), s(x0)))), y0, neg(s(x0))) at position [0,1,1] we obtained the following new rules [LPAR04]:

MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(plus_nat(s(0), x0)))), y0, pos(x0)) at position [0,1,1,0] we obtained the following new rules [LPAR04]:

MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(plus_nat(0, x0))))), y0, pos(x0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(plus_nat(0, x0))))), y0, pos(x0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, minus_nat(s(0), 0))), y0, neg(0)) at position [0,1,1] we obtained the following new rules [LPAR04]:

MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(plus_nat(0, x0))))), y0, pos(x0))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(plus_nat(0, x0))))), y0, pos(x0)) at position [0,1,1,0,0] we obtained the following new rules [LPAR04]:

MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1])))
MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [LPAR04] the rule MINUSNAT(true, x[1], y[1]) → MINUS(x[1], if(equal_int(mod_int(y[1], pos(s(s(0)))), pos(0)), y[1], plus_int(pos(s(0)), y[1]))) at position [1] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(mod_int(neg(x1), pos(s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(mod_int(pos(x1), pos(s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(mod_int(neg(x1), pos(s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(mod_int(pos(x1), pos(s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(mod_int(neg(x1), pos(s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1))) at position [1,0,0] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(mod_int(pos(x1), pos(s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))

The TRS R consists of the following rules:

mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))
mod_int(neg(x), pos(y)) → neg(mod_nat(x, y))
equal_int(pos(0), pos(0)) → true
equal_int(neg(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
and(true, false) → false
and(true, true) → true

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(mod_int(pos(x1), pos(s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(mod_int(pos(x1), pos(s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1)))) at position [1,0,0] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
mod_int(pos(x), pos(y)) → pos(mod_nat(x, y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
plus_nat(s(x), y) → s(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

mod_int(pos(x0), pos(x1))
mod_int(pos(x0), neg(x1))
mod_int(neg(x0), pos(x1))
mod_int(neg(x0), neg(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0))))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
plus_nat(s(x), y) → s(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), plus_int(pos(s(0)), pos(x0)))) at position [1,2] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, pos(x0)) → MINUS(y0, if(equal_int(pos(mod_nat(x0, s(s(0)))), pos(0)), pos(x0), pos(plus_nat(s(0), x0))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
plus_nat(s(x), y) → s(plus_nat(x, y))
if(false, u, v) → v
if(true, u, v) → u
plus_nat(0, x) → x
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0))))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), plus_int(pos(s(0)), neg(x0)))) at position [1,2] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, neg(x0)) → MINUS(y0, if(equal_int(neg(mod_nat(x0, s(s(0)))), pos(0)), neg(x0), minus_nat(s(0), x0)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
plus_int(pos(x), neg(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(plus_nat(s(0), x1)))) at position [1,2,0] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(plus_nat(0, x1)))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(plus_nat(0, x1)))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
plus_nat(s(x), y) → s(plus_nat(x, y))
plus_nat(0, x) → x
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(plus_nat(0, x1)))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
plus_nat(0, x) → x
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(plus_nat(0, x1))))) at position [1,2,0,0] we obtained the following new rules [LPAR04]:

MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
plus_nat(0, x) → x
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

plus_nat(0, x0)
plus_nat(s(x0), x1)

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ QReductionProof

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

MINUS(y0, neg(s(x0))) → MINUSNAT(and(false, equal_int(y0, minus_nat(0, x0))), y0, neg(s(x0)))

The remaining pairs can at least be oriented weakly.

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(MINUS(x₁, x₂)) = 1
POL(MINUSNAT(x₁, x₂, x₃)) = x₁
POL(and(x₁, x₂)) = x₁
POL(equal_int(x₁, x₂)) = 0
POL(false) = 0
POL(greatereq_int(x₁, x₂)) = 1
POL(if(x₁, x₂, x₃)) = 0
POL(if1(x₁, x₂, x₃)) = 0
POL(minus_nat(x₁, x₂)) = 0
POL(minus_nat_s(x₁, x₂)) = 0
POL(mod_nat(x₁, x₂)) = 0
POL(neg(x₁)) = 0
POL(pos(x₁)) = 0
POL(s(x₁)) = 0
POL(true) = 1

The following usable rules [FROCOS05] were oriented:

and(true, true) → true
and(true, false) → false
and(false, true) → false
and(false, false) → false
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ QReductionProof

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ QDPOrderProof

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ RemovalProof

                                                                                                                                              ↳ RemovalProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1)) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1))
MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
MINUS(y0, pos(x0)) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0))
MINUSNAT(true, y0, neg(x1)) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)))
MINUSNAT(true, y0, pos(x1)) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))))

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.
In the following pairs the term without variables pos(s(0)) is replaced by the fresh variable x_removed.
Pair: MINUS(y0, neg(0)) → MINUSNAT(and(true, equal_int(y0, pos(s(0)))), y0, neg(0))
Positions in right side of the pair:

[0,1,1]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ QReductionProof

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ QDPOrderProof

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ RemovalProof

                                                                                                                                                ↳ QDP

                                                                                                                                              ↳ RemovalProof

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1), x_removed) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1), x_removed)
MINUSNAT(true, y0, neg(x1), x_removed) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)), x_removed)
MINUS(y0, neg(0), x_removed) → MINUSNAT(and(true, equal_int(y0, x_removed)), y0, neg(0), x_removed)
MINUS(y0, pos(x0), x_removed) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0), x_removed)
MINUSNAT(true, y0, pos(x1), x_removed) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))), x_removed)

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

[0,1,1]

The new variable was added to all pairs as a new argument[CONREM].

↳ ITRS

  ↳ ITRStoIDPProof

    ↳ IDP

      ↳ UsableRulesProof

        ↳ IDP

          ↳ IDependencyGraphProof

            ↳ IDP

              ↳ IDPtoQDPProof

                ↳ QDP

                  ↳ UsableRulesProof

                    ↳ QDP

                      ↳ QReductionProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ UsableRulesProof

                                ↳ QDP

                                  ↳ QReductionProof

                                    ↳ QDP

                                      ↳ RemovalProof

                                      ↳ RemovalProof

                                      ↳ Narrowing

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ Rewriting

                                                        ↳ QDP

                                                          ↳ Rewriting

                                                            ↳ QDP

                                                              ↳ Rewriting

                                                                ↳ QDP

                                                                  ↳ Rewriting

                                                                    ↳ QDP

                                                                      ↳ Rewriting

                                                                        ↳ QDP

                                                                          ↳ Narrowing

                                                                            ↳ QDP

                                                                              ↳ Rewriting

                                                                                ↳ QDP

                                                                                  ↳ UsableRulesProof

                                                                                    ↳ QDP

                                                                                      ↳ Rewriting

                                                                                        ↳ QDP

                                                                                          ↳ UsableRulesProof

                                                                                            ↳ QDP

                                                                                              ↳ QReductionProof

                                                                                                ↳ QDP

                                                                                                  ↳ Rewriting

                                                                                                    ↳ QDP

                                                                                                      ↳ UsableRulesProof

                                                                                                        ↳ QDP

                                                                                                          ↳ Rewriting

                                                                                                            ↳ QDP

                                                                                                              ↳ UsableRulesProof

                                                                                                                ↳ QDP

                                                                                                                  ↳ QReductionProof

                                                                                                                    ↳ QDP

                                                                                                                      ↳ Rewriting

                                                                                                                        ↳ QDP

                                                                                                                          ↳ UsableRulesProof

                                                                                                                            ↳ QDP

                                                                                                                              ↳ Rewriting

                                                                                                                                ↳ QDP

                                                                                                                                  ↳ UsableRulesProof

                                                                                                                                    ↳ QDP

                                                                                                                                      ↳ QReductionProof

                                                                                                                                        ↳ QDP

                                                                                                                                          ↳ QDPOrderProof

                                                                                                                                            ↳ QDP

                                                                                                                                              ↳ RemovalProof

                                                                                                                                              ↳ RemovalProof

                                                                                                                                                ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MINUS(y0, neg(x1), x_removed) → MINUSNAT(and(greatereq_int(neg(x1), pos(0)), equal_int(y0, minus_nat(s(0), x1))), y0, neg(x1), x_removed)
MINUSNAT(true, y0, neg(x1), x_removed) → MINUS(y0, if(equal_int(neg(mod_nat(x1, s(s(0)))), pos(0)), neg(x1), minus_nat(s(0), x1)), x_removed)
MINUS(y0, neg(0), x_removed) → MINUSNAT(and(true, equal_int(y0, x_removed)), y0, neg(0), x_removed)
MINUS(y0, pos(x0), x_removed) → MINUSNAT(and(true, equal_int(y0, pos(s(x0)))), y0, pos(x0), x_removed)
MINUSNAT(true, y0, pos(x1), x_removed) → MINUS(y0, if(equal_int(pos(mod_nat(x1, s(s(0)))), pos(0)), pos(x1), pos(s(x1))), x_removed)

The TRS R consists of the following rules:

equal_int(pos(0), pos(s(y))) → false
equal_int(neg(0), pos(s(y))) → false
equal_int(neg(s(x)), pos(s(y))) → false
equal_int(pos(s(x)), pos(s(y))) → equal_int(pos(x), pos(y))
and(true, false) → false
and(true, true) → true
equal_int(pos(0), pos(0)) → true
equal_int(pos(s(x)), pos(0)) → false
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
equal_int(neg(0), pos(0)) → true
equal_int(neg(s(x)), pos(0)) → false
equal_int(neg(0), neg(0)) → true
equal_int(pos(0), neg(0)) → true
equal_int(pos(0), neg(s(y))) → false
equal_int(neg(0), neg(s(y))) → false
equal_int(pos(s(x)), neg(0)) → false
equal_int(neg(s(x)), neg(0)) → false
equal_int(pos(s(x)), neg(s(y))) → false
equal_int(neg(s(x)), neg(s(y))) → equal_int(neg(x), neg(y))
and(false, false) → false
and(false, true) → false
mod_nat(0, s(x)) → 0
mod_nat(s(x), s(y)) → if1(greatereq_int(pos(x), pos(y)), mod_nat(minus_nat_s(x, y), s(y)), s(x))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)
if(false, u, v) → v
if(true, u, v) → u
greatereq_int(pos(x), pos(0)) → true
greatereq_int(pos(0), pos(s(y))) → false
greatereq_int(pos(s(x)), pos(s(y))) → greatereq_int(pos(x), pos(y))
minus_nat_s(x, 0) → x
minus_nat_s(0, s(y)) → 0
minus_nat_s(s(x), s(y)) → minus_nat_s(x, y)
if1(true, x, y) → x
if1(false, x, y) → y
greatereq_int(neg(0), pos(0)) → true
greatereq_int(neg(s(x)), pos(0)) → false

The set Q consists of the following terms:

if(false, x0, x1)
if(true, x0, x1)
equal_int(pos(0), pos(0))
equal_int(neg(0), pos(0))
equal_int(neg(0), neg(0))
equal_int(pos(0), neg(0))
equal_int(pos(0), pos(s(x0)))
equal_int(neg(0), pos(s(x0)))
equal_int(pos(0), neg(s(x0)))
equal_int(neg(0), neg(s(x0)))
equal_int(pos(s(x0)), pos(0))
equal_int(pos(s(x0)), neg(0))
equal_int(neg(s(x0)), pos(0))
equal_int(neg(s(x0)), neg(0))
equal_int(pos(s(x0)), neg(s(x1)))
equal_int(neg(s(x0)), pos(s(x1)))
equal_int(pos(s(x0)), pos(s(x1)))
equal_int(neg(s(x0)), neg(s(x1)))
mod_nat(0, s(x0))
mod_nat(s(x0), s(x1))
if1(true, x0, x1)
if1(false, x0, x1)
minus_nat_s(x0, 0)
minus_nat_s(0, s(x0))
minus_nat_s(s(x0), s(x1))
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))
and(false, false)
and(false, true)
and(true, false)
and(true, true)
greatereq_int(pos(x0), pos(0))
greatereq_int(neg(0), pos(0))
greatereq_int(neg(0), neg(x0))
greatereq_int(pos(x0), neg(x1))
greatereq_int(pos(0), pos(s(x0)))
greatereq_int(neg(x0), pos(s(x1)))
greatereq_int(neg(s(x0)), pos(0))
greatereq_int(neg(s(x0)), neg(0))
greatereq_int(pos(s(x0)), pos(s(x1)))
greatereq_int(neg(s(x0)), neg(s(x1)))

We have to consider all minimal (P,Q,R)-chains.